\begin{tabbing}
st{-}key{-}match(${\it tab}$;$k_{1}$;$k_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $k_{1}$\+
\\[0ex]o\=f inl($n$) =$>$ \=case $k_{2}$\+\+
\\[0ex]o\=f inl($m$) =$>$ ff\+
\\[0ex]$\mid$ inr($a$) =$>$ ($n$ $<$z ptr(${\it tab}$) $\wedge_{b}$ $n$ $<$z $\parallel$${\it tab}$$\parallel$ ) $\wedge_{b}$ st{-}atom(${\it tab}$;$n$) =a1 $a$
\-\-\\[0ex]$\mid$ inr($a$) =$>$ \=case $k_{2}$\+
\\[0ex]o\=f inl($n$) =$>$ ($n$ $<$z ptr(${\it tab}$) $\wedge_{b}$ $n$ $<$z $\parallel$${\it tab}$$\parallel$ ) $\wedge_{b}$ st{-}atom(${\it tab}$;$n$) =a1 $a$\+
\\[0ex]$\mid$ inr($b$) =$>$ ff
\-\-\-\-
\end{tabbing}